es{-}before(${\it es}$; $e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$if es{-}first(${\it es}$; $e$)$\rightarrow$ nil else es{-}before(${\it es}$; es{-}pred(${\it es}$; $e$)) @ (es{-}pred(${\it es}$; $e$).nil) fi
\\[0ex]\emph{(recursive)}